'''
Created on 2011-05-03

@author: kacper
'''
from dataStructs.definitions import Relation
'''
Created on 2011-04-26
@author: kacper
'''
from dataStructs.formulaSet import Theory
from config.config import getAnyDatabase, testPath
from dataStructs.Transform import cnf
from test.cnf_tests import testCNF
from test.logger import instLog, instLogFun
from resolution.resolution import linearResolution

log = instLog("testTheory")
logFun = instLogFun(log)

if __name__ == '__main__':
    kb = testPath() + "/city.wn"
        
        
    print "knowledge base name ", kb
    
    th = Theory(kb)
    
    
    print " Statements in th"
    for x in th.theory:
        print x
        
    rel = 0 
    for x in th.theory:
        if  isinstance(x, Relation):
           rel =x
           break 
    
    print "our relation"
    print rel
    
    
    print "is it all right ?"
    print th.isOptymistic(str(rel))
    
    rel = rel.negFormula()
    print "negation", rel
    
    print "is it all right ?"
    try :
        print th.isOptymistic(str(rel))
    except StopIteration:
        print "max depth of iteration reached" 
  
    rel = "pl(m0,m1)"
    print "is it all right ?", rel
    print th.isOptymistic(str(rel))
    